YES 1.5 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((/=) :: (Eq a, Eq b) => (a,b ->  (a,b ->  Bool) :: (Eq a, Eq b) => (a,b ->  (a,b ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((/=) :: (Eq a, Eq b) => (a,b ->  (a,b ->  Bool) :: (Eq b, Eq a) => (a,b ->  (a,b ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((/=) :: (Eq a, Eq b) => (b,a ->  (b,a ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv2800), Succ(xv400000)) → new_primPlusNat(xv2800, xv400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30000), Succ(xv40000)) → new_primMulNat(xv30000, Succ(xv40000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_Maybe, eg)), bbh) → new_esEs(xv300, xv400, eg)
new_esEs3(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, de), app(ty_[], ea)), bbh) → new_esEs1(xv300, xv400, ea)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, hc), hd), gc, gd) → new_esEs3(xv300, xv400, hc, hd)
new_esEs3(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, de), app(app(app(ty_@3, eb), ec), ed)), bbh) → new_esEs2(xv300, xv400, eb, ec, ed)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, gc, app(ty_Maybe, bag)) → new_esEs(xv302, xv402, bag)
new_esEs(Just(xv300), Just(xv400), app(ty_Maybe, ba)) → new_esEs(xv300, xv400, ba)
new_esEs(Just(xv300), Just(xv400), app(app(app(ty_@3, be), bf), bg)) → new_esEs2(xv300, xv400, be, bf, bg)
new_esEs3(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_[], bd)), bbh) → new_esEs1(xv300, xv400, bd)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_Either, bce), bcf)) → new_esEs0(xv31, xv41, bce, bcf)
new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(app(ty_@3, fc), fd), ff)), bbh) → new_esEs2(xv300, xv400, fc, fd, ff)
new_esEs0(Right(xv300), Right(xv400), de, app(app(ty_Either, dg), dh)) → new_esEs0(xv300, xv400, dg, dh)
new_esEs(Just(xv300), Just(xv400), app(app(ty_@2, bh), ca)) → new_esEs3(xv300, xv400, bh, ca)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), app(ty_[], baa)), gd), bbh) → new_esEs1(xv301, xv401, baa)
new_esEs1(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, fg), fh)) → new_esEs3(xv300, xv400, fg, fh)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), gc), app(ty_[], bbb)), bbh) → new_esEs1(xv302, xv402, bbb)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, ge), gf)), gc), gd), bbh) → new_esEs0(xv300, xv400, ge, gf)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), gc), app(app(app(ty_@3, bbc), bbd), bbe)), bbh) → new_esEs2(xv302, xv402, bbc, bbd, bbe)
new_esEs3(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, dc), dd)), cc), bbh) → new_esEs3(xv300, xv400, dc, dd)
new_esEs0(Right(xv300), Right(xv400), de, app(ty_Maybe, df)) → new_esEs(xv300, xv400, df)
new_esEs3(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, ba)), bbh) → new_esEs(xv300, xv400, ba)
new_esEs0(Right(xv300), Right(xv400), de, app(app(app(ty_@3, eb), ec), ed)) → new_esEs2(xv300, xv400, eb, ec, ed)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, bca), bcb), bbh) → new_esEs3(xv30, xv40, bca, bcb)
new_esEs0(Right(xv300), Right(xv400), de, app(app(ty_@2, ee), ef)) → new_esEs3(xv300, xv400, ee, ef)
new_esEs3(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, bb), bc)), bbh) → new_esEs0(xv300, xv400, bb, bc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, gc, app(ty_[], bbb)) → new_esEs1(xv302, xv402, bbb)
new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_@2, fg), fh)), bbh) → new_esEs3(xv300, xv400, fg, fh)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], gg)), gc), gd), bbh) → new_esEs1(xv300, xv400, gg)
new_esEs3(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bh), ca)), bbh) → new_esEs3(xv300, xv400, bh, ca)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], gg), gc, gd) → new_esEs1(xv300, xv400, gg)
new_esEs3(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_[], cf)), cc), bbh) → new_esEs1(xv300, xv400, cf)
new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_[], fb)), bbh) → new_esEs1(xv300, xv400, fb)
new_esEs1(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, fc), fd), ff)) → new_esEs2(xv300, xv400, fc, fd, ff)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, gc, app(app(ty_Either, bah), bba)) → new_esEs0(xv302, xv402, bah, bba)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, gc, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs2(xv302, xv402, bbc, bbd, bbe)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), app(app(app(ty_@3, bab), bac), bad)), gd), bbh) → new_esEs2(xv301, xv401, bab, bac, bad)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, hc), hd)), gc), gd), bbh) → new_esEs3(xv300, xv400, hc, hd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, gh), ha), hb), gc, gd) → new_esEs2(xv300, xv400, gh, ha, hb)
new_esEs3(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, cg), da), db)), cc), bbh) → new_esEs2(xv300, xv400, cg, da, db)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(ty_Maybe, hf), gd) → new_esEs(xv301, xv401, hf)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, gb)), gc), gd), bbh) → new_esEs(xv300, xv400, gb)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs2(xv31, xv41, bch, bda, bdb)
new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], ga), bbh) → new_esEs1(xv301, xv401, ga)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ge), gf), gc, gd) → new_esEs0(xv300, xv400, ge, gf)
new_esEs1(:(xv300, xv301), :(xv400, xv401), ga) → new_esEs1(xv301, xv401, ga)
new_esEs3(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, de), app(app(ty_@2, ee), ef)), bbh) → new_esEs3(xv300, xv400, ee, ef)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(ty_[], baa), gd) → new_esEs1(xv301, xv401, baa)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), app(ty_Maybe, hf)), gd), bbh) → new_esEs(xv301, xv401, hf)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), gc), app(app(ty_Either, bah), bba)), bbh) → new_esEs0(xv302, xv402, bah, bba)
new_esEs1(:(xv300, xv301), :(xv400, xv401), app(ty_[], fb)) → new_esEs1(xv300, xv400, fb)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_[], bcg)) → new_esEs1(xv31, xv41, bcg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(ty_@2, bae), baf), gd) → new_esEs3(xv301, xv401, bae, baf)
new_esEs0(Left(xv300), Left(xv400), app(app(app(ty_@3, cg), da), db), cc) → new_esEs2(xv300, xv400, cg, da, db)
new_esEs0(Left(xv300), Left(xv400), app(app(ty_Either, cd), ce), cc) → new_esEs0(xv300, xv400, cd, ce)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), app(app(ty_@2, bae), baf)), gd), bbh) → new_esEs3(xv301, xv401, bae, baf)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, gb), gc, gd) → new_esEs(xv300, xv400, gb)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), gc), app(app(ty_@2, bbf), bbg)), bbh) → new_esEs3(xv302, xv402, bbf, bbg)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_@2, bdc), bdd)) → new_esEs3(xv31, xv41, bdc, bdd)
new_esEs(Just(xv300), Just(xv400), app(app(ty_Either, bb), bc)) → new_esEs0(xv300, xv400, bb, bc)
new_esEs1(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, eh), fa)) → new_esEs0(xv300, xv400, eh, fa)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), app(app(ty_Either, hg), hh)), gd), bbh) → new_esEs0(xv301, xv401, hg, hh)
new_esEs0(Right(xv300), Right(xv400), de, app(ty_[], ea)) → new_esEs1(xv300, xv400, ea)
new_esEs1(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, eg)) → new_esEs(xv300, xv400, eg)
new_esEs(Just(xv300), Just(xv400), app(ty_[], bd)) → new_esEs1(xv300, xv400, bd)
new_esEs3(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, de), app(ty_Maybe, df)), bbh) → new_esEs(xv300, xv400, df)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(app(ty_@3, bab), bac), bad), gd) → new_esEs2(xv301, xv401, bab, bac, bad)
new_esEs0(Left(xv300), Left(xv400), app(ty_[], cf), cc) → new_esEs1(xv300, xv400, cf)
new_esEs3(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, cb)), cc), bbh) → new_esEs(xv300, xv400, cb)
new_esEs3(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, be), bf), bg)), bbh) → new_esEs2(xv300, xv400, be, bf, bg)
new_esEs3(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_Maybe, bcd)) → new_esEs(xv31, xv41, bcd)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, he), gc), app(ty_Maybe, bag)), bbh) → new_esEs(xv302, xv402, bag)
new_esEs3(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, de), app(app(ty_Either, dg), dh)), bbh) → new_esEs0(xv300, xv400, dg, dh)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, gc, app(app(ty_@2, bbf), bbg)) → new_esEs3(xv302, xv402, bbf, bbg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), he, app(app(ty_Either, hg), hh), gd) → new_esEs0(xv301, xv401, hg, hh)
new_esEs3(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, gh), ha), hb)), gc), gd), bbh) → new_esEs2(xv300, xv400, gh, ha, hb)
new_esEs0(Left(xv300), Left(xv400), app(ty_Maybe, cb), cc) → new_esEs(xv300, xv400, cb)
new_esEs3(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, cd), ce)), cc), bbh) → new_esEs0(xv300, xv400, cd, ce)
new_esEs0(Left(xv300), Left(xv400), app(app(ty_@2, dc), dd), cc) → new_esEs3(xv300, xv400, dc, dd)
new_esEs3(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_Either, eh), fa)), bbh) → new_esEs0(xv300, xv400, eh, fa)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: